﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using OpSatPlan.PlanningGraph;
using System.Collections.ObjectModel;
using System.Diagnostics;

namespace OpSatPlan.Encoder
{
    public class EfaEncoder
    {
        private CnfEncoder mEncoder;
		private Dictionary<AtomicFormula, List<Operator>> mAddOps;
		private Dictionary<AtomicFormula, List<Operator>> mDelOps;
        public EfaEncoder(CnfEncoder encoder)
        {
            this.mEncoder = encoder;
        }

        public void Encode(IList<Operator> operators, List<AtomicFormula> allVars)
        {
			this.mAddOps = new Dictionary<AtomicFormula, List<Operator>>();
			this.mDelOps = new Dictionary<AtomicFormula, List<Operator>>();
			List<Operator> ops;

			foreach(Operator op in operators)
			{
				foreach(ReadOnlyCollection<AtomicFormula> rAfs in op.AddEffects)
				{
					foreach(AtomicFormula af in rAfs)
					{
						if(this.mAddOps.ContainsKey(af))
							ops = this.mAddOps[af];
						else
						{
							ops = new List<Operator>();
							this.mAddOps.Add(af, ops);
						}
						ops.Add(op);
					}
				}
				foreach(ReadOnlyCollection<AtomicFormula> rAfs in op.DeleteEffects)
				{
					foreach(AtomicFormula af in rAfs)
					{
						if(this.mDelOps.ContainsKey(af))
							ops = this.mDelOps[af];
						else
						{
							ops = new List<Operator>();
							this.mDelOps.Add(af, ops);
						}
						ops.Add(op);
					}
				}
			}
			
			var trans = from af in allVars
                           select new { vafp = new ValuedAtomicFormula(af, true), vafn = new ValuedAtomicFormula(af, false) };
			
            foreach (var tran in trans)
            {
                this.EncodeTruthChange(tran.vafp, tran.vafn, operators);
                this.EncodeTruthChange(tran.vafn, tran.vafp, operators);
            }
        }

        private void EncodeTruthChange(ValuedAtomicFormula start, ValuedAtomicFormula end, IList<Operator> operators)
        {
            List<Operator> ops;
			IEnumerable<KeyValuePair<Action, Operator>> acts;
            if(!end.Value)
            {
				if(this.mDelOps.ContainsKey(end.AtomicFormula))
				{
	                ops = this.mDelOps[end.AtomicFormula];
					
					acts = from op in ops
	                       from act in op.Actions
	                       where act.ContainsDeleteEffect(end.AtomicFormula)
	                       select new KeyValuePair<Action, Operator>(act, op);
				}
				else
				{
					if(end.AtomicFormula.Definition.Name == "FUEL-LEVEL")
					{
						// logistics domain 
						ops = (from op in operators
								where op.Actions.Any(a => a.ActionDefinition.Name == "ZOOM" ||
														a.ActionDefinition.Name == "FLY" ||
														a.ActionDefinition.Name == "REFUEL")
								select op).ToList();
						acts = from op in ops
	                       from act in op.Actions
	                       where act.ContainsDeleteEffect(end.AtomicFormula)
	                       select new KeyValuePair<Action, Operator>(act, op);
					}
					else
					{
						ops = new List<Operator>();
						acts = new List<KeyValuePair<Action, Operator>>();
					}
				}
            }
            else
            {
				if(this.mAddOps.ContainsKey(end.AtomicFormula))
				{
	                ops = this.mAddOps[end.AtomicFormula];
					
					acts = from op in ops
	                       from act in op.Actions
	                       where act.ContainsAddEffect(end.AtomicFormula)
	                       select new KeyValuePair<Action, Operator>(act, op);
				}
				else
				{
					if(end.AtomicFormula.Definition.Name == "FUEL-LEVEL")
					{
						// logistics domain
						ops = (from op in operators
								where op.Actions.Any(a => a.ActionDefinition.Name == "ZOOM" ||
														a.ActionDefinition.Name == "FLY" ||
														a.ActionDefinition.Name == "REFUEL")
								select op).ToList();
						acts = from op in ops
	                       from act in op.Actions
	                       where act.ContainsAddEffect(end.AtomicFormula)
	                       select new KeyValuePair<Action, Operator>(act, op);
					}
					else
					{
						ops = new List<Operator>();
						acts = new List<KeyValuePair<Action, Operator>>();
					}
				}
            }
			this.TruthChangeImpliesOperators(ops, start, end);
			if(ops.Count != 0)
			{
				this.TruthChangeImpliesFirstIdentifier(ops, acts, start, end);
	            this.TruthChangeAfterFirstIdentifier(ops, acts, start, end);
	            this.TruthChangeDrillDown(ops, acts, start, end);	
			}
        }

        private void TruthChangeImpliesOperators(IEnumerable<Operator> ops, ValuedAtomicFormula start, ValuedAtomicFormula end)
        {
            ClauseTemplate clause;
            clause = new ClauseTemplate(this.mEncoder);

            clause.Add(start.AtomicFormula, 0, !start.Value);
            clause.Add(end.AtomicFormula, 1, !end.Value);

            foreach (Operator op in ops)
            {
                clause.Add(op, true);
            }
            this.mEncoder.WriteClauses(clause);
        }
        private void TruthChangeDrillDown(IEnumerable<Operator> ops, IEnumerable<KeyValuePair<Action, Operator>> acts, ValuedAtomicFormula start, ValuedAtomicFormula end)
        {

            ClauseTemplate clause;

            foreach (var pair in acts)
            {
                Identifier id;
                for (int i = 1; i < pair.Key.Identifiers.Count; i++)
                {
                    Identifier idTemp = null;
                    
                    clause = new ClauseTemplate(this.mEncoder);
                    clause.Add(start.AtomicFormula, 0, !start.Value);
                    clause.Add(end.AtomicFormula, 1, !end.Value);
                    clause.Add(pair.Value, false);
                    for (int j = 0; j < i; j++)
                    {
                        id = pair.Key.Identifiers[j];
                        clause.Add(id.AtomicFormula, (id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1), !id.Value);
                    }
                    
					if(end.AtomicFormula.Definition.Name == "FUEL-LEVEL")
					{
					}
					
					id = pair.Key.Identifiers[i];

                    clause.Add(id.AtomicFormula, (id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1), id.Value);
					
					
                    List<Identifier> ids = new List<Identifier>();
                    for (int j = 0; j < i; j++)
                    {
                        ids.Add(pair.Key.Identifiers[j]);
                    }
                    IEnumerable<Action> res;
                    if (!end.Value)
                    {
						if(end.AtomicFormula.Definition.Name == "FUEL-LEVEL" &&
							id.AtomicFormula.Definition.Name == "FUEL-LEVEL")
							// specific to logistics domain.
							res = from op in ops
									from act in op.Actions
                              where ids.All(k => act.ContainsIdentifier(k))
                              //&& act.ContainsDeleteEffect(end.AtomicFormula)
                              select act;
						else
                        	res = from act in pair.Value.Actions
                              	where ids.All(k => act.ContainsIdentifier(k))
                              	&& act.ContainsDeleteEffect(end.AtomicFormula)
                              	select act;
                    }
                    else
                    {
						if(end.AtomicFormula.Definition.Name == "FUEL-LEVEL" &&
							id.AtomicFormula.Definition.Name == "FUEL-LEVEL")
							// specific to logistics domain
							res = from op in ops
									from act in op.Actions
                              where ids.All(k => act.ContainsIdentifier(k))
                              //&& act.ContainsAddEffect(end.AtomicFormula)
                              select act;
						else
                        	res = from act in pair.Value.Actions
                              where ids.All(k => act.ContainsIdentifier(k))
                              && act.ContainsAddEffect(end.AtomicFormula)
                              select act;
                    }

                    foreach (Action a in res)
                    {
                        idTemp = null;
						List<Identifier> idRes;
						
						idRes = a.GetMatching(id);
                        if (idRes != null && idRes.Count > 0)
                        {
							foreach(Identifier ik in idRes)
							{
								if(id.AtomicFormula.Arguments.All(o => ik.AtomicFormula.Arguments[id.AtomicFormula.Arguments.IndexOf(o)].Type == o.Type))
								{
	                       			idTemp  = ik;
	                    			break;
								}
							}
                        }
//                        else
//                        {
//                            var idRes2 = from x in
//                                             (from ik in a.Identifiers
//                                              where ik.IdentifierType == id.IdentifierType &&
//                                                     ik.Value == id.Value &&
//                                                     ik.AtomicFormula.Arguments.Any(o => id.AtomicFormula.Arguments.Contains(o))
//                                              select ik)
//                                         where x != null
//                                         select x;
//                            if (idRes2 != null && idRes2.Count() > 0)
//                            {
//                                idTemp = (Identifier)idRes2.ElementAt(0);
//                            }
//                        }
                        if (idTemp != null)
                        {
                            clause.Add(idTemp.AtomicFormula, (idTemp.IdentifierType == IdentifierTypes.Precondition ? 0 : 1), idTemp.Value);
                        }
                    }
                    this.mEncoder.WriteClauses(clause);
                }
            }
        }
        private void TruthChangeAfterFirstIdentifier(IEnumerable<Operator> ops, IEnumerable<KeyValuePair<Action, Operator>> acts, 
													ValuedAtomicFormula start, ValuedAtomicFormula end)
        {
            Dictionary<string, string> seen = new Dictionary<string, string>();
            ClauseTemplate clause;

            foreach (KeyValuePair<Action, Operator> act in acts)
            {
                Identifier id = act.Key.Identifiers[0];
                clause = new ClauseTemplate(this.mEncoder);

                clause.Add(start.AtomicFormula, 0, !start.Value);
                clause.Add(end.AtomicFormula, 1, !end.Value);
                clause.Add(id.AtomicFormula, (id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1), !id.Value);
				
                if (!seen.ContainsKey(clause.GenerateClause(0)))
                {
                    seen.Add(clause.GenerateClause(0), clause.GenerateClause(0));
                }
                else
                    continue;
                var ops2 = from x in
                               (from op in ops
                                from a in op.Actions
                                where a.ContainsIdentifier(id)
                                select op)
                           where x != null
                           select x;
                foreach (Operator op in ops2)
                {
                    clause.Add(op, true);
                }
                this.mEncoder.WriteClauses(clause);
            }
        }

        private void TruthChangeImpliesFirstIdentifier(IEnumerable<Operator> ops, IEnumerable<KeyValuePair<Action, Operator>> acts,
														ValuedAtomicFormula start, ValuedAtomicFormula end)
        {
            ClauseTemplate clause;

            clause = new ClauseTemplate(this.mEncoder);
            clause.Add(start.AtomicFormula, 0, !start.Value);
            clause.Add(end.AtomicFormula, 1, !end.Value);

          
            foreach (KeyValuePair<Action, Operator> act in acts)
            {
                Identifier id = act.Key.Identifiers[0];
                clause.Add(id.AtomicFormula, (id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1), id.Value);
            }
            this.mEncoder.WriteClauses(clause);
        }

    }
}
